import {pipe, zip, every, makeContinuable, take} from './iterator.js'
import {isSubtypeOf, type Type} from './type.js'
import type {BracketFunctionSpecification, FunctionSpecification} from './functionSpecification.js'
import {serializeList} from './serializeList.js'

export type VariableSpecification = {
    name: string
    type: Type
}

export type MetaMap = Map<MetaVariableTerm, Term>
export type BoundMap = Map<QuantifiedVariableTerm, QuantifiedVariableTerm>

export abstract class Term {
    abstract getType(): Type

    substitute(map: Map<Term, Term>): Term {
        const mappedTerm = map.get(this)

        return mappedTerm
            ? mappedTerm.substitute(map)
            : this
    }

    abstract unify(other: Term, metaMap: MetaMap, boundMap: BoundMap): boolean
    abstract serialize(): Iterable<string>

    static unifyLists(terms1: Term[], terms2: Term[], metaMap: MetaMap, boundMap: BoundMap) {
        return terms1.length == terms2.length &&
            pipe(
                zip(terms1, terms2),
                every(([term1, term2]) => term1.unify(term2, metaMap, boundMap)),
            )
    }
}

export abstract class VariableTerm extends Term {
    name: string
    type: Type

    constructor({name, type}: VariableSpecification) {
        super()
        this.name = name
        this.type = type
    }

    getType() {
        return this.type
    }

    * serialize(): Iterable<string> {
        yield this.name
    }
}

export class QuantifiedVariableTerm extends VariableTerm {
    unify(other: Term, metaMap: MetaMap, boundMap: BoundMap): boolean {
        return this === other || boundMap.get(this) == other
    }
}

export class FreeVariableTerm extends VariableTerm {
    unify(other: Term, metaMap: MetaMap, boundMap: BoundMap): boolean {
        if (this === other)
            return true

        if (other instanceof MetaVariableTerm && isSubtypeOf(this.type, other.type)) {
            metaMap.set(other, this)
            return true
        }

        return false
    }
}

export class MetaVariableTerm extends VariableTerm {
    unify(other: Term, metaMap: MetaMap, boundMap: BoundMap): boolean {
        if (this === other)
            return true

        {
            const actualTerm = metaMap.get(this)

            if (actualTerm)
                return actualTerm.unify(other, metaMap, boundMap)
        }

        if (other instanceof MetaVariableTerm) {
            {
                const actualTerm = metaMap.get(other)

                if (actualTerm)
                    return this.unify(actualTerm, metaMap, boundMap)
            }

            if (isSubtypeOf(other.type, this.type))
                metaMap.set(this, other)
            else // if (isSubtypeOf(this.type, other.type))    TODO is this needed?
                metaMap.set(other, this)

            return true
        }

        return other.unify(this, metaMap, boundMap)
    }
}

export class FunctionTerm extends Term {
    specification: FunctionSpecification
    parameters: Term[]

    constructor(specification: FunctionSpecification, parameters: Term[]) {
        super()
        this.specification = specification
        this.parameters = parameters
    }

    getType() {
        return this.specification.type
    }

    substitute(map: Map<Term, Term>): Term {
        const mappedTerm = map.get(this)

        return mappedTerm
            ? mappedTerm.substitute(map)
            : new FunctionTerm(this.specification, this.parameters.map(term => term.substitute(map)))
    }

    unify(other: Term, metaMap: MetaMap, boundMap: BoundMap): boolean {
        if (this === other)
            return true

        if (other instanceof QuantifiedVariableTerm)
            return false

        if (other instanceof MetaVariableTerm) {
            const term2_ = metaMap.get(other)

            if (term2_)
                return this.unify(term2_, metaMap, boundMap)
        }

        if (other instanceof FunctionTerm && this.specification === other.specification)
            return Term.unifyLists(this.parameters, other.parameters, metaMap, boundMap)

        if (!(other instanceof MetaVariableTerm) || !isSubtypeOf(this.specification.type, other.type))
            return false

        metaMap.set(other, this)
        return true
    }

    // TODO fix function serialization to respect precedence
    * serialize(): Iterable<string> {
        if ('left' in this.specification) {
            yield* serializeBracketTerm(this.specification, this.parameters)
            return
        }

        const {length} = this.specification.parameterTypes
        const parameterIterator = makeContinuable(this.parameters)

        const {symbolOffset} = this.specification

        if (symbolOffset > 1)
            yield '('

        yield* serializeList(
            take(symbolOffset)(parameterIterator),
            serialize,
        )

        if (symbolOffset > 1)
            yield ')'

        if (symbolOffset > 0)
            yield ' '

        yield this.specification.name

        if (length > symbolOffset)
            yield ' '

        if (length - symbolOffset > 1)
            yield '('

        yield* serializeList(parameterIterator, serialize)

        if (length - symbolOffset > 1)
            yield ')'
    }
}

const serialize = (term: Term) => term.serialize()

function* serializeBracketTerm(
    {left, right}: BracketFunctionSpecification,
    parameters: Iterable<Term>,
): Iterable<string> {
    yield left
    yield ' '

    yield* serializeList(parameters, serialize)

    yield ' '
    yield right
}
